Nuprl Lemma : s-filter_wf
11,40
postcript
pdf
T
:Type,
as
:(
T
List),
P
:({
a
:
T
| (
a
as
)}
). (
T
r
)
(s-filter(
P
;
as
)
(
T
List))
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
(
x
l
)
,
P
Q
,
s-insert(
x
;
l
)
,
if
b
then
t
else
f
fi
,
reduce(
f
;
k
;
as
)
,
s-filter(
p
;
as
)
,
Lemmas
bool
wf
,
list-subtype
,
reduce
wf
,
ifthenelse
wf
,
s-insert
wf
,
l
member
wf
origin
T:Type, as:(T List), P:({a:T| (a 
as)} 
). (T 
r 
) 
(s-filter(P;as) (T List)) T:Type, as:(T List), P:({a:T| (a as)} ). (T r ) (s-filter(P;as) (T List)) Tx:A. B(x) l) Q